poss:(ES{i}{i'}), R:(possible-event{i:l}(poss)possible-event{i:l}(poss){i'}).
(e:possible-event{i:l}(poss). R(e,e))
 (P:(possible-event{i:l}(poss){i'}), e:possible-event{i:l}(poss).
 es-knows{i:l}(poss; R; P; e)  (P(e))) 

latex

Definitions	t  T, x:A. B(x), x:AB(x), x:A  B(x), PossibleEvent(poss), f(a), P  Q, Type, , ES, K(P)@e
Lemmas	possible-event wf, event system wf